Termination w.r.t. Q proof of /tmp/tmpIvrNWo/cime2.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(a, s), t) → MSUBST(a, t)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(a, s), t) → MSUBST(a, t)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(a, s), t) → MSUBST(a, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)

The remaining pairs can at least be oriented weakly.

CIRC(circ(s, t), u) → CIRC(t, u)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))

Used ordering: Polynomial interpretation [25]:

POL(CIRC(x₁, x₂)) = x₁ + x₁·x₂ + x₂
POL(MSUBST(x₁, x₂)) = x₁ + x₁·x₂ + x₂
POL(circ(x₁, x₂)) = x₁ + x₁·x₂ + x₂
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(id) = 1
POL(lift) = 1
POL(msubst(x₁, x₂)) = x₁ + x₁·x₂ + x₂

The following usable rules [17] were oriented:

circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(id, s) → s
circ(s, id) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
msubst(msubst(a, s), t) → msubst(a, circ(s, t))
msubst(a, id) → a

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(t, u)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
The graph contains the following edges 1 > 1
CIRC(circ(s, t), u) → CIRC(t, u)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

From the DPs we obtained the following set of size-change graphs:

MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
The graph contains the following edges 1 > 1